\begin{tabbing}
$\forall$${\it es}$:ES, ${\it Sys}$:AbsInterface(Top), $f$:sys{-}antecedent(${\it es}$;${\it Sys}$).
\\[0ex]fifo{-}antecedent(${\it es}$;${\it Sys}$;$f$)
\\[0ex]$\Rightarrow$ \=($\forall$$a$, $b$:E(${\it Sys}$).\+
\\[0ex](loc($a$) = loc($b$) $\in$ Id)
\\[0ex]$\Rightarrow$ (loc($f$($a$)) = loc($f$($b$)) $\in$ Id)
\\[0ex]$\Rightarrow$ \{($f$($a$) $<$loc $f$($b$)) $\Leftarrow\!\Rightarrow$ ($a$ $<$loc $b$)\})
\-
\end{tabbing}